초보자를 위한 AVISPA 간단 정리

AVISPA란 프로토콜의 안전성을 검증하는데 쓰이는 HLPSL언어이다.

AVISPA

• Avispa는 baisc role, session role, environment role이 존재한다.
• environment role은 다른 프로그래밍 언어의 main 함수를 의미한다.
• session role은 environment에서 basic role을 불러오는데 쓰이는 함수이다.
• basic role은 실제 기능을 수행하는 함수라 보면된다.

AVISPA을 프로그래밍 하면서 주의할점

! avispa는 컴파일시 코드를 읽는 순서가 존재한다.

• top down 형식이 아닌, down-top 형태로 읽는다. 즉, environment role이 맨아래, session role, basic role 순으로 존재해야한다.

  주의! 맨 위에서부터 environment role -> session role -> basic role 순서로 짜면, session role undefined error가 나옴.
  
  

• 다음은 session role에서 인자값으로 초기값을 정의 할 경우에 해당하는 문제
  
  

• 보통 role session(A,B:agent, Ka,Kb:symmetric_key) 이런식으로 정의하는데, 이때 모든 인자의 첫 문자는 대문자 알파벳을 가져야함.

  • 소문자로 시작하여 선언해봤는데, identy error
    
    

• session role(A,B:agent)로 선언했을 시,

  • played_by A에서 agent로 선언한 A를 뜻함. 즉, role session(player1, player2:agent)라고 선언하면 player_by plater1 이런식으로 선언해주어야 에러가 안난다.
    
    

• text 변수 선언시, 언더바(_)를 넣으면 이후에 곤란해진다.

  • transition 부분에서는 언더바(_)는 암호화됨을 뜻한다.
  • 변수를 읽는 과정에서 _때문에 암호되는 부분이라 처리해버리고, 그로인해 정상적인 변수명을 읽어올 수 없음
    
    

• SND_AB(A,B,{Ni,Mi}_K)처럼, A->B로 간다는 부분에서는 쉼표(,)를 써줘야한다.

  • 암호화된 부분 {Ni, Mi}에서는 점(.)을 써줘야한다.
  • 암호화 부분에서 콤마를 쓰면 바로 에러로 즉결